Left Termination of the query pattern
query(g)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 UndefinedPredicateHandlerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 46 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 136 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 TRUE

(0) Obligation:

Clauses:

query(.(C1, .(D1, .(C2, .(D2, []))))) :- ','(density(C1, D1), ','(density(C2, D2), ','(>(D1, D2), ','(is(T1, *(20, D1)), ','(is(T2, *(21, D2)), <(T1, T2)))))).
density(C, D) :- ','(pop(C, P), ','(area(C, A), is(D, /(*(P, 100), A)))).
pop(china, 8250).
area(china, 3380).
pop(india, 5863).
area(india, 1139).
pop(ussr, 2521).
area(ussr, 8708).
pop(usa, 2119).
area(usa, 3609).
pop(indonesia, 1276).
area(indonesia, 570).
pop(japan, 1097).
area(japan, 148).
pop(brazil, 1042).
area(brazil, 3288).
pop(bangladesh, 750).
area(bangladesh, 55).
pop(pakistan, 682).
area(pakistan, 311).
pop(w_germany, 620).
area(w_germany, 96).
pop(nigeria, 613).
area(nigeria, 373).
pop(mexico, 581).
area(mexico, 764).
pop(uk, 559).
area(uk, 86).
pop(italy, 554).
area(italy, 116).
pop(france, 525).
area(france, 213).
pop(phillipines, 415).
area(phillipines, 90).
pop(thailand, 410).
area(thailand, 200).
pop(turkey, 383).
area(turkey, 296).
pop(egypt, 364).
area(egypt, 386).
pop(spain, 352).
area(spain, 190).
pop(poland, 337).
area(poland, 121).
pop(s_korea, 335).
area(s_korea, 37).
pop(iran, 320).
area(iran, 628).
pop(ethiopia, 272).
area(ethiopia, 350).
pop(argentina, 251).
area(argentina, 1080).

Query: query(g)

(1) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(2) Obligation:

Clauses:

query(.(C1, .(D1, .(C2, .(D2, []))))) :- ','(density(C1, D1), ','(density(C2, D2), ','(>(D1, D2), ','(is(T1, *(20, D1)), ','(is(T2, *(21, D2)), <(T1, T2)))))).
density(C, D) :- ','(pop(C, P), ','(area(C, A), is(D, /(*(P, 100), A)))).
pop(china, 8250).
area(china, 3380).
pop(india, 5863).
area(india, 1139).
pop(ussr, 2521).
area(ussr, 8708).
pop(usa, 2119).
area(usa, 3609).
pop(indonesia, 1276).
area(indonesia, 570).
pop(japan, 1097).
area(japan, 148).
pop(brazil, 1042).
area(brazil, 3288).
pop(bangladesh, 750).
area(bangladesh, 55).
pop(pakistan, 682).
area(pakistan, 311).
pop(w_germany, 620).
area(w_germany, 96).
pop(nigeria, 613).
area(nigeria, 373).
pop(mexico, 581).
area(mexico, 764).
pop(uk, 559).
area(uk, 86).
pop(italy, 554).
area(italy, 116).
pop(france, 525).
area(france, 213).
pop(phillipines, 415).
area(phillipines, 90).
pop(thailand, 410).
area(thailand, 200).
pop(turkey, 383).
area(turkey, 296).
pop(egypt, 364).
area(egypt, 386).
pop(spain, 352).
area(spain, 190).
pop(poland, 337).
area(poland, 121).
pop(s_korea, 335).
area(s_korea, 37).
pop(iran, 320).
area(iran, 628).
pop(ethiopia, 272).
area(ethiopia, 350).
pop(argentina, 251).
area(argentina, 1080).
>(X0, X1).
is(X0, X1).
<(X0, X1).

Query: query(g)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
query_in: (b)
density_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

query_in_g(.(C1, .(D1, .(C2, .(D2, []))))) → U1_g(C1, D1, C2, D2, density_in_gg(C1, D1))
density_in_gg(C, D) → U7_gg(C, D, pop_in_ga(C, P))
pop_in_ga(china, 8250) → pop_out_ga(china, 8250)
pop_in_ga(india, 5863) → pop_out_ga(india, 5863)
pop_in_ga(ussr, 2521) → pop_out_ga(ussr, 2521)
pop_in_ga(usa, 2119) → pop_out_ga(usa, 2119)
pop_in_ga(indonesia, 1276) → pop_out_ga(indonesia, 1276)
pop_in_ga(japan, 1097) → pop_out_ga(japan, 1097)
pop_in_ga(brazil, 1042) → pop_out_ga(brazil, 1042)
pop_in_ga(bangladesh, 750) → pop_out_ga(bangladesh, 750)
pop_in_ga(pakistan, 682) → pop_out_ga(pakistan, 682)
pop_in_ga(w_germany, 620) → pop_out_ga(w_germany, 620)
pop_in_ga(nigeria, 613) → pop_out_ga(nigeria, 613)
pop_in_ga(mexico, 581) → pop_out_ga(mexico, 581)
pop_in_ga(uk, 559) → pop_out_ga(uk, 559)
pop_in_ga(italy, 554) → pop_out_ga(italy, 554)
pop_in_ga(france, 525) → pop_out_ga(france, 525)
pop_in_ga(phillipines, 415) → pop_out_ga(phillipines, 415)
pop_in_ga(thailand, 410) → pop_out_ga(thailand, 410)
pop_in_ga(turkey, 383) → pop_out_ga(turkey, 383)
pop_in_ga(egypt, 364) → pop_out_ga(egypt, 364)
pop_in_ga(spain, 352) → pop_out_ga(spain, 352)
pop_in_ga(poland, 337) → pop_out_ga(poland, 337)
pop_in_ga(s_korea, 335) → pop_out_ga(s_korea, 335)
pop_in_ga(iran, 320) → pop_out_ga(iran, 320)
pop_in_ga(ethiopia, 272) → pop_out_ga(ethiopia, 272)
pop_in_ga(argentina, 251) → pop_out_ga(argentina, 251)
U7_gg(C, D, pop_out_ga(C, P)) → U8_gg(C, D, P, area_in_ga(C, A))
area_in_ga(china, 3380) → area_out_ga(china, 3380)
area_in_ga(india, 1139) → area_out_ga(india, 1139)
area_in_ga(ussr, 8708) → area_out_ga(ussr, 8708)
area_in_ga(usa, 3609) → area_out_ga(usa, 3609)
area_in_ga(indonesia, 570) → area_out_ga(indonesia, 570)
area_in_ga(japan, 148) → area_out_ga(japan, 148)
area_in_ga(brazil, 3288) → area_out_ga(brazil, 3288)
area_in_ga(bangladesh, 55) → area_out_ga(bangladesh, 55)
area_in_ga(pakistan, 311) → area_out_ga(pakistan, 311)
area_in_ga(w_germany, 96) → area_out_ga(w_germany, 96)
area_in_ga(nigeria, 373) → area_out_ga(nigeria, 373)
area_in_ga(mexico, 764) → area_out_ga(mexico, 764)
area_in_ga(uk, 86) → area_out_ga(uk, 86)
area_in_ga(italy, 116) → area_out_ga(italy, 116)
area_in_ga(france, 213) → area_out_ga(france, 213)
area_in_ga(phillipines, 90) → area_out_ga(phillipines, 90)
area_in_ga(thailand, 200) → area_out_ga(thailand, 200)
area_in_ga(turkey, 296) → area_out_ga(turkey, 296)
area_in_ga(egypt, 386) → area_out_ga(egypt, 386)
area_in_ga(spain, 190) → area_out_ga(spain, 190)
area_in_ga(poland, 121) → area_out_ga(poland, 121)
area_in_ga(s_korea, 37) → area_out_ga(s_korea, 37)
area_in_ga(iran, 628) → area_out_ga(iran, 628)
area_in_ga(ethiopia, 350) → area_out_ga(ethiopia, 350)
area_in_ga(argentina, 1080) → area_out_ga(argentina, 1080)
U8_gg(C, D, P, area_out_ga(C, A)) → U9_gg(C, D, is_in_gg(D, /(*(P, 100), A)))
is_in_gg(X0, X1) → is_out_gg(X0, X1)
U9_gg(C, D, is_out_gg(D, /(*(P, 100), A))) → density_out_gg(C, D)
U1_g(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_g(C1, D1, C2, D2, density_in_gg(C2, D2))
U2_g(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_g(C1, D1, C2, D2, >_in_gg(D1, D2))
>_in_gg(X0, X1) → >_out_gg(X0, X1)
U3_g(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_g(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U4_g(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_g(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U5_g(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_g(C1, D1, C2, D2, <_in_aa(T1, T2))
<_in_aa(X0, X1) → <_out_aa(X0, X1)
U6_g(C1, D1, C2, D2, <_out_aa(T1, T2)) → query_out_g(.(C1, .(D1, .(C2, .(D2, [])))))

The argument filtering Pi contains the following mapping:
query_in_g(x1)  =  query_in_g(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U1_g(x1, x2, x3, x4, x5)  =  U1_g(x2, x3, x4, x5)
density_in_gg(x1, x2)  =  density_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
pop_in_ga(x1, x2)  =  pop_in_ga(x1)
china  =  china
pop_out_ga(x1, x2)  =  pop_out_ga(x2)
india  =  india
ussr  =  ussr
usa  =  usa
indonesia  =  indonesia
japan  =  japan
brazil  =  brazil
bangladesh  =  bangladesh
pakistan  =  pakistan
w_germany  =  w_germany
nigeria  =  nigeria
mexico  =  mexico
uk  =  uk
italy  =  italy
france  =  france
phillipines  =  phillipines
thailand  =  thailand
turkey  =  turkey
egypt  =  egypt
spain  =  spain
poland  =  poland
s_korea  =  s_korea
iran  =  iran
ethiopia  =  ethiopia
argentina  =  argentina
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
area_in_ga(x1, x2)  =  area_in_ga(x1)
area_out_ga(x1, x2)  =  area_out_ga(x2)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
is_in_gg(x1, x2)  =  is_in_gg(x1, x2)
is_out_gg(x1, x2)  =  is_out_gg
/(x1, x2)  =  /(x1, x2)
*(x1, x2)  =  *(x1, x2)
100  =  100
density_out_gg(x1, x2)  =  density_out_gg
U2_g(x1, x2, x3, x4, x5)  =  U2_g(x2, x4, x5)
U3_g(x1, x2, x3, x4, x5)  =  U3_g(x2, x4, x5)
>_in_gg(x1, x2)  =  >_in_gg(x1, x2)
>_out_gg(x1, x2)  =  >_out_gg
U4_g(x1, x2, x3, x4, x5)  =  U4_g(x4, x5)
is_in_ag(x1, x2)  =  is_in_ag(x2)
is_out_ag(x1, x2)  =  is_out_ag
20  =  20
U5_g(x1, x2, x3, x4, x5, x6)  =  U5_g(x6)
21  =  21
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
<_in_aa(x1, x2)  =  <_in_aa
<_out_aa(x1, x2)  =  <_out_aa
query_out_g(x1)  =  query_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

query_in_g(.(C1, .(D1, .(C2, .(D2, []))))) → U1_g(C1, D1, C2, D2, density_in_gg(C1, D1))
density_in_gg(C, D) → U7_gg(C, D, pop_in_ga(C, P))
pop_in_ga(china, 8250) → pop_out_ga(china, 8250)
pop_in_ga(india, 5863) → pop_out_ga(india, 5863)
pop_in_ga(ussr, 2521) → pop_out_ga(ussr, 2521)
pop_in_ga(usa, 2119) → pop_out_ga(usa, 2119)
pop_in_ga(indonesia, 1276) → pop_out_ga(indonesia, 1276)
pop_in_ga(japan, 1097) → pop_out_ga(japan, 1097)
pop_in_ga(brazil, 1042) → pop_out_ga(brazil, 1042)
pop_in_ga(bangladesh, 750) → pop_out_ga(bangladesh, 750)
pop_in_ga(pakistan, 682) → pop_out_ga(pakistan, 682)
pop_in_ga(w_germany, 620) → pop_out_ga(w_germany, 620)
pop_in_ga(nigeria, 613) → pop_out_ga(nigeria, 613)
pop_in_ga(mexico, 581) → pop_out_ga(mexico, 581)
pop_in_ga(uk, 559) → pop_out_ga(uk, 559)
pop_in_ga(italy, 554) → pop_out_ga(italy, 554)
pop_in_ga(france, 525) → pop_out_ga(france, 525)
pop_in_ga(phillipines, 415) → pop_out_ga(phillipines, 415)
pop_in_ga(thailand, 410) → pop_out_ga(thailand, 410)
pop_in_ga(turkey, 383) → pop_out_ga(turkey, 383)
pop_in_ga(egypt, 364) → pop_out_ga(egypt, 364)
pop_in_ga(spain, 352) → pop_out_ga(spain, 352)
pop_in_ga(poland, 337) → pop_out_ga(poland, 337)
pop_in_ga(s_korea, 335) → pop_out_ga(s_korea, 335)
pop_in_ga(iran, 320) → pop_out_ga(iran, 320)
pop_in_ga(ethiopia, 272) → pop_out_ga(ethiopia, 272)
pop_in_ga(argentina, 251) → pop_out_ga(argentina, 251)
U7_gg(C, D, pop_out_ga(C, P)) → U8_gg(C, D, P, area_in_ga(C, A))
area_in_ga(china, 3380) → area_out_ga(china, 3380)
area_in_ga(india, 1139) → area_out_ga(india, 1139)
area_in_ga(ussr, 8708) → area_out_ga(ussr, 8708)
area_in_ga(usa, 3609) → area_out_ga(usa, 3609)
area_in_ga(indonesia, 570) → area_out_ga(indonesia, 570)
area_in_ga(japan, 148) → area_out_ga(japan, 148)
area_in_ga(brazil, 3288) → area_out_ga(brazil, 3288)
area_in_ga(bangladesh, 55) → area_out_ga(bangladesh, 55)
area_in_ga(pakistan, 311) → area_out_ga(pakistan, 311)
area_in_ga(w_germany, 96) → area_out_ga(w_germany, 96)
area_in_ga(nigeria, 373) → area_out_ga(nigeria, 373)
area_in_ga(mexico, 764) → area_out_ga(mexico, 764)
area_in_ga(uk, 86) → area_out_ga(uk, 86)
area_in_ga(italy, 116) → area_out_ga(italy, 116)
area_in_ga(france, 213) → area_out_ga(france, 213)
area_in_ga(phillipines, 90) → area_out_ga(phillipines, 90)
area_in_ga(thailand, 200) → area_out_ga(thailand, 200)
area_in_ga(turkey, 296) → area_out_ga(turkey, 296)
area_in_ga(egypt, 386) → area_out_ga(egypt, 386)
area_in_ga(spain, 190) → area_out_ga(spain, 190)
area_in_ga(poland, 121) → area_out_ga(poland, 121)
area_in_ga(s_korea, 37) → area_out_ga(s_korea, 37)
area_in_ga(iran, 628) → area_out_ga(iran, 628)
area_in_ga(ethiopia, 350) → area_out_ga(ethiopia, 350)
area_in_ga(argentina, 1080) → area_out_ga(argentina, 1080)
U8_gg(C, D, P, area_out_ga(C, A)) → U9_gg(C, D, is_in_gg(D, /(*(P, 100), A)))
is_in_gg(X0, X1) → is_out_gg(X0, X1)
U9_gg(C, D, is_out_gg(D, /(*(P, 100), A))) → density_out_gg(C, D)
U1_g(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_g(C1, D1, C2, D2, density_in_gg(C2, D2))
U2_g(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_g(C1, D1, C2, D2, >_in_gg(D1, D2))
>_in_gg(X0, X1) → >_out_gg(X0, X1)
U3_g(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_g(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U4_g(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_g(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U5_g(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_g(C1, D1, C2, D2, <_in_aa(T1, T2))
<_in_aa(X0, X1) → <_out_aa(X0, X1)
U6_g(C1, D1, C2, D2, <_out_aa(T1, T2)) → query_out_g(.(C1, .(D1, .(C2, .(D2, [])))))

The argument filtering Pi contains the following mapping:
query_in_g(x1)  =  query_in_g(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U1_g(x1, x2, x3, x4, x5)  =  U1_g(x2, x3, x4, x5)
density_in_gg(x1, x2)  =  density_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
pop_in_ga(x1, x2)  =  pop_in_ga(x1)
china  =  china
pop_out_ga(x1, x2)  =  pop_out_ga(x2)
india  =  india
ussr  =  ussr
usa  =  usa
indonesia  =  indonesia
japan  =  japan
brazil  =  brazil
bangladesh  =  bangladesh
pakistan  =  pakistan
w_germany  =  w_germany
nigeria  =  nigeria
mexico  =  mexico
uk  =  uk
italy  =  italy
france  =  france
phillipines  =  phillipines
thailand  =  thailand
turkey  =  turkey
egypt  =  egypt
spain  =  spain
poland  =  poland
s_korea  =  s_korea
iran  =  iran
ethiopia  =  ethiopia
argentina  =  argentina
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
area_in_ga(x1, x2)  =  area_in_ga(x1)
area_out_ga(x1, x2)  =  area_out_ga(x2)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
is_in_gg(x1, x2)  =  is_in_gg(x1, x2)
is_out_gg(x1, x2)  =  is_out_gg
/(x1, x2)  =  /(x1, x2)
*(x1, x2)  =  *(x1, x2)
100  =  100
density_out_gg(x1, x2)  =  density_out_gg
U2_g(x1, x2, x3, x4, x5)  =  U2_g(x2, x4, x5)
U3_g(x1, x2, x3, x4, x5)  =  U3_g(x2, x4, x5)
>_in_gg(x1, x2)  =  >_in_gg(x1, x2)
>_out_gg(x1, x2)  =  >_out_gg
U4_g(x1, x2, x3, x4, x5)  =  U4_g(x4, x5)
is_in_ag(x1, x2)  =  is_in_ag(x2)
is_out_ag(x1, x2)  =  is_out_ag
20  =  20
U5_g(x1, x2, x3, x4, x5, x6)  =  U5_g(x6)
21  =  21
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
<_in_aa(x1, x2)  =  <_in_aa
<_out_aa(x1, x2)  =  <_out_aa
query_out_g(x1)  =  query_out_g

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

QUERY_IN_G(.(C1, .(D1, .(C2, .(D2, []))))) → U1_G(C1, D1, C2, D2, density_in_gg(C1, D1))
QUERY_IN_G(.(C1, .(D1, .(C2, .(D2, []))))) → DENSITY_IN_GG(C1, D1)
DENSITY_IN_GG(C, D) → U7_GG(C, D, pop_in_ga(C, P))
DENSITY_IN_GG(C, D) → POP_IN_GA(C, P)
U7_GG(C, D, pop_out_ga(C, P)) → U8_GG(C, D, P, area_in_ga(C, A))
U7_GG(C, D, pop_out_ga(C, P)) → AREA_IN_GA(C, A)
U8_GG(C, D, P, area_out_ga(C, A)) → U9_GG(C, D, is_in_gg(D, /(*(P, 100), A)))
U8_GG(C, D, P, area_out_ga(C, A)) → IS_IN_GG(D, /(*(P, 100), A))
U1_G(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_G(C1, D1, C2, D2, density_in_gg(C2, D2))
U1_G(C1, D1, C2, D2, density_out_gg(C1, D1)) → DENSITY_IN_GG(C2, D2)
U2_G(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_G(C1, D1, C2, D2, >_in_gg(D1, D2))
U2_G(C1, D1, C2, D2, density_out_gg(C2, D2)) → >_IN_GG(D1, D2)
U3_G(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_G(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
U3_G(C1, D1, C2, D2, >_out_gg(D1, D2)) → IS_IN_AG(T1, *(20, D1))
U4_G(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_G(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U4_G(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → IS_IN_AG(T2, *(21, D2))
U5_G(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_G(C1, D1, C2, D2, <_in_aa(T1, T2))
U5_G(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → <_IN_AA(T1, T2)

The TRS R consists of the following rules:

query_in_g(.(C1, .(D1, .(C2, .(D2, []))))) → U1_g(C1, D1, C2, D2, density_in_gg(C1, D1))
density_in_gg(C, D) → U7_gg(C, D, pop_in_ga(C, P))
pop_in_ga(china, 8250) → pop_out_ga(china, 8250)
pop_in_ga(india, 5863) → pop_out_ga(india, 5863)
pop_in_ga(ussr, 2521) → pop_out_ga(ussr, 2521)
pop_in_ga(usa, 2119) → pop_out_ga(usa, 2119)
pop_in_ga(indonesia, 1276) → pop_out_ga(indonesia, 1276)
pop_in_ga(japan, 1097) → pop_out_ga(japan, 1097)
pop_in_ga(brazil, 1042) → pop_out_ga(brazil, 1042)
pop_in_ga(bangladesh, 750) → pop_out_ga(bangladesh, 750)
pop_in_ga(pakistan, 682) → pop_out_ga(pakistan, 682)
pop_in_ga(w_germany, 620) → pop_out_ga(w_germany, 620)
pop_in_ga(nigeria, 613) → pop_out_ga(nigeria, 613)
pop_in_ga(mexico, 581) → pop_out_ga(mexico, 581)
pop_in_ga(uk, 559) → pop_out_ga(uk, 559)
pop_in_ga(italy, 554) → pop_out_ga(italy, 554)
pop_in_ga(france, 525) → pop_out_ga(france, 525)
pop_in_ga(phillipines, 415) → pop_out_ga(phillipines, 415)
pop_in_ga(thailand, 410) → pop_out_ga(thailand, 410)
pop_in_ga(turkey, 383) → pop_out_ga(turkey, 383)
pop_in_ga(egypt, 364) → pop_out_ga(egypt, 364)
pop_in_ga(spain, 352) → pop_out_ga(spain, 352)
pop_in_ga(poland, 337) → pop_out_ga(poland, 337)
pop_in_ga(s_korea, 335) → pop_out_ga(s_korea, 335)
pop_in_ga(iran, 320) → pop_out_ga(iran, 320)
pop_in_ga(ethiopia, 272) → pop_out_ga(ethiopia, 272)
pop_in_ga(argentina, 251) → pop_out_ga(argentina, 251)
U7_gg(C, D, pop_out_ga(C, P)) → U8_gg(C, D, P, area_in_ga(C, A))
area_in_ga(china, 3380) → area_out_ga(china, 3380)
area_in_ga(india, 1139) → area_out_ga(india, 1139)
area_in_ga(ussr, 8708) → area_out_ga(ussr, 8708)
area_in_ga(usa, 3609) → area_out_ga(usa, 3609)
area_in_ga(indonesia, 570) → area_out_ga(indonesia, 570)
area_in_ga(japan, 148) → area_out_ga(japan, 148)
area_in_ga(brazil, 3288) → area_out_ga(brazil, 3288)
area_in_ga(bangladesh, 55) → area_out_ga(bangladesh, 55)
area_in_ga(pakistan, 311) → area_out_ga(pakistan, 311)
area_in_ga(w_germany, 96) → area_out_ga(w_germany, 96)
area_in_ga(nigeria, 373) → area_out_ga(nigeria, 373)
area_in_ga(mexico, 764) → area_out_ga(mexico, 764)
area_in_ga(uk, 86) → area_out_ga(uk, 86)
area_in_ga(italy, 116) → area_out_ga(italy, 116)
area_in_ga(france, 213) → area_out_ga(france, 213)
area_in_ga(phillipines, 90) → area_out_ga(phillipines, 90)
area_in_ga(thailand, 200) → area_out_ga(thailand, 200)
area_in_ga(turkey, 296) → area_out_ga(turkey, 296)
area_in_ga(egypt, 386) → area_out_ga(egypt, 386)
area_in_ga(spain, 190) → area_out_ga(spain, 190)
area_in_ga(poland, 121) → area_out_ga(poland, 121)
area_in_ga(s_korea, 37) → area_out_ga(s_korea, 37)
area_in_ga(iran, 628) → area_out_ga(iran, 628)
area_in_ga(ethiopia, 350) → area_out_ga(ethiopia, 350)
area_in_ga(argentina, 1080) → area_out_ga(argentina, 1080)
U8_gg(C, D, P, area_out_ga(C, A)) → U9_gg(C, D, is_in_gg(D, /(*(P, 100), A)))
is_in_gg(X0, X1) → is_out_gg(X0, X1)
U9_gg(C, D, is_out_gg(D, /(*(P, 100), A))) → density_out_gg(C, D)
U1_g(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_g(C1, D1, C2, D2, density_in_gg(C2, D2))
U2_g(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_g(C1, D1, C2, D2, >_in_gg(D1, D2))
>_in_gg(X0, X1) → >_out_gg(X0, X1)
U3_g(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_g(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U4_g(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_g(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U5_g(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_g(C1, D1, C2, D2, <_in_aa(T1, T2))
<_in_aa(X0, X1) → <_out_aa(X0, X1)
U6_g(C1, D1, C2, D2, <_out_aa(T1, T2)) → query_out_g(.(C1, .(D1, .(C2, .(D2, [])))))

The argument filtering Pi contains the following mapping:
query_in_g(x1)  =  query_in_g(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U1_g(x1, x2, x3, x4, x5)  =  U1_g(x2, x3, x4, x5)
density_in_gg(x1, x2)  =  density_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
pop_in_ga(x1, x2)  =  pop_in_ga(x1)
china  =  china
pop_out_ga(x1, x2)  =  pop_out_ga(x2)
india  =  india
ussr  =  ussr
usa  =  usa
indonesia  =  indonesia
japan  =  japan
brazil  =  brazil
bangladesh  =  bangladesh
pakistan  =  pakistan
w_germany  =  w_germany
nigeria  =  nigeria
mexico  =  mexico
uk  =  uk
italy  =  italy
france  =  france
phillipines  =  phillipines
thailand  =  thailand
turkey  =  turkey
egypt  =  egypt
spain  =  spain
poland  =  poland
s_korea  =  s_korea
iran  =  iran
ethiopia  =  ethiopia
argentina  =  argentina
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
area_in_ga(x1, x2)  =  area_in_ga(x1)
area_out_ga(x1, x2)  =  area_out_ga(x2)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
is_in_gg(x1, x2)  =  is_in_gg(x1, x2)
is_out_gg(x1, x2)  =  is_out_gg
/(x1, x2)  =  /(x1, x2)
*(x1, x2)  =  *(x1, x2)
100  =  100
density_out_gg(x1, x2)  =  density_out_gg
U2_g(x1, x2, x3, x4, x5)  =  U2_g(x2, x4, x5)
U3_g(x1, x2, x3, x4, x5)  =  U3_g(x2, x4, x5)
>_in_gg(x1, x2)  =  >_in_gg(x1, x2)
>_out_gg(x1, x2)  =  >_out_gg
U4_g(x1, x2, x3, x4, x5)  =  U4_g(x4, x5)
is_in_ag(x1, x2)  =  is_in_ag(x2)
is_out_ag(x1, x2)  =  is_out_ag
20  =  20
U5_g(x1, x2, x3, x4, x5, x6)  =  U5_g(x6)
21  =  21
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
<_in_aa(x1, x2)  =  <_in_aa
<_out_aa(x1, x2)  =  <_out_aa
query_out_g(x1)  =  query_out_g
QUERY_IN_G(x1)  =  QUERY_IN_G(x1)
U1_G(x1, x2, x3, x4, x5)  =  U1_G(x2, x3, x4, x5)
DENSITY_IN_GG(x1, x2)  =  DENSITY_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
POP_IN_GA(x1, x2)  =  POP_IN_GA(x1)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)
AREA_IN_GA(x1, x2)  =  AREA_IN_GA(x1)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
IS_IN_GG(x1, x2)  =  IS_IN_GG(x1, x2)
U2_G(x1, x2, x3, x4, x5)  =  U2_G(x2, x4, x5)
U3_G(x1, x2, x3, x4, x5)  =  U3_G(x2, x4, x5)
>_IN_GG(x1, x2)  =  >_IN_GG(x1, x2)
U4_G(x1, x2, x3, x4, x5)  =  U4_G(x4, x5)
IS_IN_AG(x1, x2)  =  IS_IN_AG(x2)
U5_G(x1, x2, x3, x4, x5, x6)  =  U5_G(x6)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x5)
<_IN_AA(x1, x2)  =  <_IN_AA

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUERY_IN_G(.(C1, .(D1, .(C2, .(D2, []))))) → U1_G(C1, D1, C2, D2, density_in_gg(C1, D1))
QUERY_IN_G(.(C1, .(D1, .(C2, .(D2, []))))) → DENSITY_IN_GG(C1, D1)
DENSITY_IN_GG(C, D) → U7_GG(C, D, pop_in_ga(C, P))
DENSITY_IN_GG(C, D) → POP_IN_GA(C, P)
U7_GG(C, D, pop_out_ga(C, P)) → U8_GG(C, D, P, area_in_ga(C, A))
U7_GG(C, D, pop_out_ga(C, P)) → AREA_IN_GA(C, A)
U8_GG(C, D, P, area_out_ga(C, A)) → U9_GG(C, D, is_in_gg(D, /(*(P, 100), A)))
U8_GG(C, D, P, area_out_ga(C, A)) → IS_IN_GG(D, /(*(P, 100), A))
U1_G(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_G(C1, D1, C2, D2, density_in_gg(C2, D2))
U1_G(C1, D1, C2, D2, density_out_gg(C1, D1)) → DENSITY_IN_GG(C2, D2)
U2_G(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_G(C1, D1, C2, D2, >_in_gg(D1, D2))
U2_G(C1, D1, C2, D2, density_out_gg(C2, D2)) → >_IN_GG(D1, D2)
U3_G(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_G(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
U3_G(C1, D1, C2, D2, >_out_gg(D1, D2)) → IS_IN_AG(T1, *(20, D1))
U4_G(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_G(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U4_G(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → IS_IN_AG(T2, *(21, D2))
U5_G(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_G(C1, D1, C2, D2, <_in_aa(T1, T2))
U5_G(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → <_IN_AA(T1, T2)

The TRS R consists of the following rules:

query_in_g(.(C1, .(D1, .(C2, .(D2, []))))) → U1_g(C1, D1, C2, D2, density_in_gg(C1, D1))
density_in_gg(C, D) → U7_gg(C, D, pop_in_ga(C, P))
pop_in_ga(china, 8250) → pop_out_ga(china, 8250)
pop_in_ga(india, 5863) → pop_out_ga(india, 5863)
pop_in_ga(ussr, 2521) → pop_out_ga(ussr, 2521)
pop_in_ga(usa, 2119) → pop_out_ga(usa, 2119)
pop_in_ga(indonesia, 1276) → pop_out_ga(indonesia, 1276)
pop_in_ga(japan, 1097) → pop_out_ga(japan, 1097)
pop_in_ga(brazil, 1042) → pop_out_ga(brazil, 1042)
pop_in_ga(bangladesh, 750) → pop_out_ga(bangladesh, 750)
pop_in_ga(pakistan, 682) → pop_out_ga(pakistan, 682)
pop_in_ga(w_germany, 620) → pop_out_ga(w_germany, 620)
pop_in_ga(nigeria, 613) → pop_out_ga(nigeria, 613)
pop_in_ga(mexico, 581) → pop_out_ga(mexico, 581)
pop_in_ga(uk, 559) → pop_out_ga(uk, 559)
pop_in_ga(italy, 554) → pop_out_ga(italy, 554)
pop_in_ga(france, 525) → pop_out_ga(france, 525)
pop_in_ga(phillipines, 415) → pop_out_ga(phillipines, 415)
pop_in_ga(thailand, 410) → pop_out_ga(thailand, 410)
pop_in_ga(turkey, 383) → pop_out_ga(turkey, 383)
pop_in_ga(egypt, 364) → pop_out_ga(egypt, 364)
pop_in_ga(spain, 352) → pop_out_ga(spain, 352)
pop_in_ga(poland, 337) → pop_out_ga(poland, 337)
pop_in_ga(s_korea, 335) → pop_out_ga(s_korea, 335)
pop_in_ga(iran, 320) → pop_out_ga(iran, 320)
pop_in_ga(ethiopia, 272) → pop_out_ga(ethiopia, 272)
pop_in_ga(argentina, 251) → pop_out_ga(argentina, 251)
U7_gg(C, D, pop_out_ga(C, P)) → U8_gg(C, D, P, area_in_ga(C, A))
area_in_ga(china, 3380) → area_out_ga(china, 3380)
area_in_ga(india, 1139) → area_out_ga(india, 1139)
area_in_ga(ussr, 8708) → area_out_ga(ussr, 8708)
area_in_ga(usa, 3609) → area_out_ga(usa, 3609)
area_in_ga(indonesia, 570) → area_out_ga(indonesia, 570)
area_in_ga(japan, 148) → area_out_ga(japan, 148)
area_in_ga(brazil, 3288) → area_out_ga(brazil, 3288)
area_in_ga(bangladesh, 55) → area_out_ga(bangladesh, 55)
area_in_ga(pakistan, 311) → area_out_ga(pakistan, 311)
area_in_ga(w_germany, 96) → area_out_ga(w_germany, 96)
area_in_ga(nigeria, 373) → area_out_ga(nigeria, 373)
area_in_ga(mexico, 764) → area_out_ga(mexico, 764)
area_in_ga(uk, 86) → area_out_ga(uk, 86)
area_in_ga(italy, 116) → area_out_ga(italy, 116)
area_in_ga(france, 213) → area_out_ga(france, 213)
area_in_ga(phillipines, 90) → area_out_ga(phillipines, 90)
area_in_ga(thailand, 200) → area_out_ga(thailand, 200)
area_in_ga(turkey, 296) → area_out_ga(turkey, 296)
area_in_ga(egypt, 386) → area_out_ga(egypt, 386)
area_in_ga(spain, 190) → area_out_ga(spain, 190)
area_in_ga(poland, 121) → area_out_ga(poland, 121)
area_in_ga(s_korea, 37) → area_out_ga(s_korea, 37)
area_in_ga(iran, 628) → area_out_ga(iran, 628)
area_in_ga(ethiopia, 350) → area_out_ga(ethiopia, 350)
area_in_ga(argentina, 1080) → area_out_ga(argentina, 1080)
U8_gg(C, D, P, area_out_ga(C, A)) → U9_gg(C, D, is_in_gg(D, /(*(P, 100), A)))
is_in_gg(X0, X1) → is_out_gg(X0, X1)
U9_gg(C, D, is_out_gg(D, /(*(P, 100), A))) → density_out_gg(C, D)
U1_g(C1, D1, C2, D2, density_out_gg(C1, D1)) → U2_g(C1, D1, C2, D2, density_in_gg(C2, D2))
U2_g(C1, D1, C2, D2, density_out_gg(C2, D2)) → U3_g(C1, D1, C2, D2, >_in_gg(D1, D2))
>_in_gg(X0, X1) → >_out_gg(X0, X1)
U3_g(C1, D1, C2, D2, >_out_gg(D1, D2)) → U4_g(C1, D1, C2, D2, is_in_ag(T1, *(20, D1)))
is_in_ag(X0, X1) → is_out_ag(X0, X1)
U4_g(C1, D1, C2, D2, is_out_ag(T1, *(20, D1))) → U5_g(C1, D1, C2, D2, T1, is_in_ag(T2, *(21, D2)))
U5_g(C1, D1, C2, D2, T1, is_out_ag(T2, *(21, D2))) → U6_g(C1, D1, C2, D2, <_in_aa(T1, T2))
<_in_aa(X0, X1) → <_out_aa(X0, X1)
U6_g(C1, D1, C2, D2, <_out_aa(T1, T2)) → query_out_g(.(C1, .(D1, .(C2, .(D2, [])))))

The argument filtering Pi contains the following mapping:
query_in_g(x1)  =  query_in_g(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
U1_g(x1, x2, x3, x4, x5)  =  U1_g(x2, x3, x4, x5)
density_in_gg(x1, x2)  =  density_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
pop_in_ga(x1, x2)  =  pop_in_ga(x1)
china  =  china
pop_out_ga(x1, x2)  =  pop_out_ga(x2)
india  =  india
ussr  =  ussr
usa  =  usa
indonesia  =  indonesia
japan  =  japan
brazil  =  brazil
bangladesh  =  bangladesh
pakistan  =  pakistan
w_germany  =  w_germany
nigeria  =  nigeria
mexico  =  mexico
uk  =  uk
italy  =  italy
france  =  france
phillipines  =  phillipines
thailand  =  thailand
turkey  =  turkey
egypt  =  egypt
spain  =  spain
poland  =  poland
s_korea  =  s_korea
iran  =  iran
ethiopia  =  ethiopia
argentina  =  argentina
U8_gg(x1, x2, x3, x4)  =  U8_gg(x2, x3, x4)
area_in_ga(x1, x2)  =  area_in_ga(x1)
area_out_ga(x1, x2)  =  area_out_ga(x2)
U9_gg(x1, x2, x3)  =  U9_gg(x3)
is_in_gg(x1, x2)  =  is_in_gg(x1, x2)
is_out_gg(x1, x2)  =  is_out_gg
/(x1, x2)  =  /(x1, x2)
*(x1, x2)  =  *(x1, x2)
100  =  100
density_out_gg(x1, x2)  =  density_out_gg
U2_g(x1, x2, x3, x4, x5)  =  U2_g(x2, x4, x5)
U3_g(x1, x2, x3, x4, x5)  =  U3_g(x2, x4, x5)
>_in_gg(x1, x2)  =  >_in_gg(x1, x2)
>_out_gg(x1, x2)  =  >_out_gg
U4_g(x1, x2, x3, x4, x5)  =  U4_g(x4, x5)
is_in_ag(x1, x2)  =  is_in_ag(x2)
is_out_ag(x1, x2)  =  is_out_ag
20  =  20
U5_g(x1, x2, x3, x4, x5, x6)  =  U5_g(x6)
21  =  21
U6_g(x1, x2, x3, x4, x5)  =  U6_g(x5)
<_in_aa(x1, x2)  =  <_in_aa
<_out_aa(x1, x2)  =  <_out_aa
query_out_g(x1)  =  query_out_g
QUERY_IN_G(x1)  =  QUERY_IN_G(x1)
U1_G(x1, x2, x3, x4, x5)  =  U1_G(x2, x3, x4, x5)
DENSITY_IN_GG(x1, x2)  =  DENSITY_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
POP_IN_GA(x1, x2)  =  POP_IN_GA(x1)
U8_GG(x1, x2, x3, x4)  =  U8_GG(x2, x3, x4)
AREA_IN_GA(x1, x2)  =  AREA_IN_GA(x1)
U9_GG(x1, x2, x3)  =  U9_GG(x3)
IS_IN_GG(x1, x2)  =  IS_IN_GG(x1, x2)
U2_G(x1, x2, x3, x4, x5)  =  U2_G(x2, x4, x5)
U3_G(x1, x2, x3, x4, x5)  =  U3_G(x2, x4, x5)
>_IN_GG(x1, x2)  =  >_IN_GG(x1, x2)
U4_G(x1, x2, x3, x4, x5)  =  U4_G(x4, x5)
IS_IN_AG(x1, x2)  =  IS_IN_AG(x2)
U5_G(x1, x2, x3, x4, x5, x6)  =  U5_G(x6)
U6_G(x1, x2, x3, x4, x5)  =  U6_G(x5)
<_IN_AA(x1, x2)  =  <_IN_AA

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 0 SCCs with 18 less nodes.

(8) TRUE